fischer-inv{i:l,
fischer-inv{$x:ut2,
fischer-inv{$try:ut2,
fischer-inv{$taken:ut2,
fischer-inv{$contending:ut2,
fischer-inv{$free:ut2,
fischer-inv{$mine:ut2,
fischer-inv{$wanted:ut2,
fischer-inv{$z:ut2}
fischer-inv(es; L; del; e)
== ((es-after(es; mkid{$x:ut2}; e) = mkid{$mine:ut2})
==  (l_all(L;
==  (l_all(Id;
==  (l_all(j.(((j = loc(e)))
==  (l_all( e'@j.f-event{$x:ut2}
==  (l_all( e'@j.f-event(es; L; e')
==  (l_all( e'@j. (f-round{i:l}
==  (l_all( e'@j. (f-round(mkid{$x:ut2}; mkid{$free:ut2}; es; e')
==  (l_all( e'@j. (=
==  (l_all( e'@j. (f-round{i:l}
==  (l_all( e'@j. (f-round(mkid{$x:ut2}; mkid{$free:ut2}; es; e))
==  (l_all( e'@j. (es-after(es; mkid{$x:ut2}; e') = mkid{$taken:ut2})
==  (l_all( e'@j. alle-at(es;
==  (l_all( e'@j. alle-at(j;
==  (l_all( e'@j. alle-at(e''.((f-round{i:l}
==  (l_all( e'@j. alle-at(e''.((f-round(mkid{$x:ut2}; mkid{$free:ut2}; es; e''
==  (l_all( e'@j. alle-at(e''.((f-round()  f-round{i:l}
==  (l_all( e'@j. alle-at(e''.((f-round()  f-round(mkid{$x:ut2}; mkid{$free:ut2}; es; e'))
==  (l_all( e'@j. alle-at( es-le(es; e''; e')))))
==   (e':es-E(es). 
==   f-event{$x:ut2}
==   f-event(es; L; e')
==    (f-round{i:l}
==    (f-round(mkid{$x:ut2}; mkid{$free:ut2}; es; e')  f-round{i:l}
==    (f-round(mkid{$x:ut2}; mkid{$free:ut2}; es; e')  f-round(mkid{$x:ut2};
==    (f-round(mkid{$x:ut2}; mkid{$free:ut2}; es; e')  f-round(mkid{$free:ut2};
==    (f-round(mkid{$x:ut2}; mkid{$free:ut2}; es; e')  f-round(es;
==    (f-round(mkid{$x:ut2}; mkid{$free:ut2}; es; e')  f-round(e))
==    (qle((es-time(es; e') + del); es-time(es; e))  (e' = e)))))
==  (f-newround{$x:ut2, $free:ut2, $mine:ut2}
==  (f-newround(es; L; e)
==   (e':es-E(es). 
==   (loc(e')  L)
==    @e'(mkid{$x:ut2}mkid{$free:ut2})
==    ((loc(e') = loc(e)))
==    (es-isrcv(es; e'))
==    (es-tag(es; e') = mkid{$free:ut2})
==    (es-lnk(es; e') = <loc(e), loc(e'), mkid{$z:ut2}>)
==    (es-sender(es; e') = e)
==    (f-rank{i:l}
==    (f-rank(mkid{$x:ut2}; mkid{$free:ut2}; es; e')
==    (=
==    (f-rank{i:l}
==    (f-rank(mkid{$x:ut2}; mkid{$free:ut2}; es; e))))
==  (@e(mkid{$x:ut2}mkid{$try:ut2})
==   (e':es-E(es). 
==   ((loc(e') = loc(e)))
==    (es-isrcv(es; e'))
==    (es-tag(es; e') = mkid{$wanted:ut2})
==    (es-lnk(es; e') = <loc(e), loc(e'), mkid{$z:ut2}>)
==    (es-sender(es; e') = e)
==    ((@e'(mkid{$x:ut2}mkid{$taken:ut2})
==     (f-rank{i:l}
==     (f-rank(mkid{$x:ut2}; mkid{$free:ut2}; es; e')
==     (=
==     (f-rank{i:l}
==     (f-rank(mkid{$x:ut2}; mkid{$free:ut2}; es; e)))
==     (@e'(mkid{$x:ut2}mkid{$contending:ut2})
==      (f-rank{i:l}
==      (f-rank(mkid{$x:ut2}; mkid{$free:ut2}; es; e')
==      (=
==      (inc-snd(f-rank{i:l}(mkid{$x:ut2}; mkid{$free:ut2}; es; e)))))))
==  (e':es-E(es). 
==  f-event{$x:ut2}
==  f-event(es; L; e')
==   (f-rank{i:l}
==   (f-rank(mkid{$x:ut2}; mkid{$free:ut2}; es; e')
==   (=
==   (f-rank{i:l}
==   (f-rank(mkid{$x:ut2}; mkid{$free:ut2}; es; e))
==   qle(qdist(es-time(es; e); es-time(es; e')); del)) 

latex

---

clarification:

fischer-inv{i:l,
fischer-inv{$x:ut2,
fischer-inv{$try:ut2,
fischer-inv{$taken:ut2,
fischer-inv{$contending:ut2,
fischer-inv{$free:ut2,
fischer-inv{$mine:ut2,
fischer-inv{$wanted:ut2,
fischer-inv{$z:ut2}
fischer-inv(es; L; del; e)
== ((es-after(es; mkid{$x:ut2}; e) = mkid{$mine:ut2}  Id)
==  (l_all(L;
==  (l_all(Id;
==  (l_all(j.(((j = es-loc(es; e)  Id))
==  (l_all( existse-at(es;
==  (l_all( existse-at(j;
==  (l_all( existse-at(e'.(f-event{$x:ut2}
==  (l_all( existse-at(e'.(f-event(es; L; e')
==  (l_all( existse-at( (f-round{i:l}
==  (l_all( existse-at( (f-round(mkid{$x:ut2}; mkid{$free:ut2}; es; e')
==  (l_all( existse-at( (=
==  (l_all( existse-at( (f-round{i:l}
==  (l_all( existse-at( (f-round(mkid{$x:ut2}; mkid{$free:ut2}; es; e)
==  (l_all( existse-at( ( )
==  (l_all( existse-at( (es-after(es; mkid{$x:ut2}; e') = mkid{$taken:ut2}  Id)
==  (l_all( existse-at( alle-at(es;
==  (l_all( existse-at( alle-at(j;
==  (l_all( existse-at( alle-at(e''.((f-round{i:l}
==  (l_all( existse-at( alle-at(e''.((f-round(mkid{$x:ut2}; mkid{$free:ut2}; es; e''
==  (l_all( existse-at( alle-at(e''.((f-round()  f-round{i:l}
==  (l_all( existse-at( alle-at(e''.((f-round()  f-round(mkid{$x:ut2}; mkid{$free:ut2}; es; e'
==  (l_all( existse-at( alle-at(e''.((f-round()  f-round())
==  (l_all( existse-at( alle-at( es-le(es; e''; e')))))))
==   (e':es-E(es). 
==   f-event{$x:ut2}
==   f-event(es; L; e')
==    (f-round{i:l}
==    (f-round(mkid{$x:ut2}; mkid{$free:ut2}; es; e')  f-round{i:l}
==    (f-round(mkid{$x:ut2}; mkid{$free:ut2}; es; e')  f-round(mkid{$x:ut2};
==    (f-round(mkid{$x:ut2}; mkid{$free:ut2}; es; e')  f-round(mkid{$free:ut2};
==    (f-round(mkid{$x:ut2}; mkid{$free:ut2}; es; e')  f-round(es;
==    (f-round(mkid{$x:ut2}; mkid{$free:ut2}; es; e')  f-round(e))
==    (qle((es-time(es; e') + del); es-time(es; e))  (e' = e  es-E(es))))))
==  (f-newround{$x:ut2, $free:ut2, $mine:ut2}
==  (f-newround(es; L; e)
==   (e':es-E(es). 
==   (es-loc(es; e')  L  Id)
==    es-change-to(es;Id;mkid{$x:ut2};e';mkid{$free:ut2})
==    ((es-loc(es; e') = es-loc(es; e)  Id))
==    (es-isrcv(es; e'))
==    (es-tag(es; e') = mkid{$free:ut2}  Id)
==    (es-lnk(es; e') = <es-loc(es; e), es-loc(es; e'), mkid{$z:ut2}>  IdLnk)
==    (es-sender(es; e') = e  es-E(es))
==    (f-rank{i:l}
==    (f-rank(mkid{$x:ut2}; mkid{$free:ut2}; es; e')
==    (=
==    (f-rank{i:l}
==    (f-rank(mkid{$x:ut2}; mkid{$free:ut2}; es; e)
==    ( (:  ))))
==  (es-change-to(es;Id;mkid{$x:ut2};e;mkid{$try:ut2})
==   (e':es-E(es). 
==   ((es-loc(es; e') = es-loc(es; e)  Id))
==    (es-isrcv(es; e'))
==    (es-tag(es; e') = mkid{$wanted:ut2}  Id)
==    (es-lnk(es; e') = <es-loc(es; e), es-loc(es; e'), mkid{$z:ut2}>  IdLnk)
==    (es-sender(es; e') = e  es-E(es))
==    ((es-change-to(es;Id;mkid{$x:ut2};e';mkid{$taken:ut2})
==     (f-rank{i:l}
==     (f-rank(mkid{$x:ut2}; mkid{$free:ut2}; es; e')
==     (=
==     (f-rank{i:l}
==     (f-rank(mkid{$x:ut2}; mkid{$free:ut2}; es; e)
==     ( (:  )))
==     (es-change-to(es;Id;mkid{$x:ut2};e';mkid{$contending:ut2})
==      (f-rank{i:l}
==      (f-rank(mkid{$x:ut2}; mkid{$free:ut2}; es; e')
==      (=
==      (inc-snd(f-rank{i:l}(mkid{$x:ut2}; mkid{$free:ut2}; es; e))
==      ( (:  ))))))
==  (e':es-E(es). 
==  f-event{$x:ut2}
==  f-event(es; L; e')
==   (f-rank{i:l}
==   (f-rank(mkid{$x:ut2}; mkid{$free:ut2}; es; e')
==   (=
==   (f-rank{i:l}
==   (f-rank(mkid{$x:ut2}; mkid{$free:ut2}; es; e)
==   ( (:  ))
==   qle(qdist(es-time(es; e); es-time(es; e')); del)) 

latex

Definitions

l_all(L; T; x.P(x)), e@i.P(e), es-after(es; x; e), alle-at(es; i; e.P(e)), es-le(es; e; e'), A  B, f-round{i:l}(x; free; es; e), P  Q, r + s, f-newround{$x:ut2, $free:ut2, $mine:ut2}(es; L; e), (x  l), A, b, es-isrcv(es; e), es-tag(es; e), IdLnk, es-lnk(es; e), <a, b>, loc(e), es-sender(es; e), P  Q, @e(xv), Id, inc-snd(p), x:A. B(x), es-E(es), f-event{$x:ut2}(es; L; e), P  Q, s = t, x:A  B(x), , f-rank{i:l}(x; free; es; e), mkid{$x:ut2}, qle(r; s), qdist(r; s), es-time(es; e)

FDL editor aliases

fischer-inv